let X be set ; :: thesis: for x being Element of (BooleLatt X) holds x ` = X \ x
set B = BooleLatt X;
let x be Element of (BooleLatt X); :: thesis: x ` = X \ x
A1: (x `) "/\" x = Bottom (BooleLatt X) by LATTICES:20;
A2: x "\/" (x `) = Top (BooleLatt X) by LATTICES:21;
A3: Bottom (BooleLatt X) = {} by Th3;
A4: Top (BooleLatt X) = X by Th4;
A5: x ` misses x by A1, A3;
A6: X \ x = (x \ x) \/ ((x `) \ x) by A2, A4, XBOOLE_1:42;
x \ x = {} by XBOOLE_1:37;
hence x ` = X \ x by A5, A6, XBOOLE_1:83; :: thesis: verum