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

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