let L be non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr ; :: thesis: L is Boolean Lattice
ex c being Element of L st
for a being Element of L holds
( c "\/" a = a & a "\/" c = a )

proof

consider b being Element of L;
take c = (b | (b | b)) | (b | (b | b)); :: thesis: for a being Element of L holds
( c "\/" a = a & a "\/" c = a )
let a be Element of L; :: thesis: ( c "\/" a = a & a "\/" c = a )
thus c "\/" a = a :: thesis: a "\/" c = a

proof

c "\/" a = (((b | (b | b)) " ) " ) | (a | a) by Def12
.= (((a | (a | a)) " ) " ) | (a | a) by Th33
.= (a | (a | a)) | (a | a) by Def13
.= (a | a) | (a | (a | a)) by Th32
.= (a | a) | (a | a) by Def14
.= a by Def13 ;
hence c "\/" a = a ; :: thesis: verum

end;

thus a "\/" c = a :: thesis: verum

proof

a "\/" c = (a | a) | (((b | (b | b)) " ) " ) by Def12
.= (a | a) | (((a | (a | a)) " ) " ) by Th33
.= (a | a) | (a | (a | a)) by Def13
.= (a | a) | (a | a) by Def14
.= a by Def13 ;
hence a "\/" c = a ; :: thesis: verum

end;

end;

then A1: L is lower-bounded' by Def3;
ex c being Element of L st
for a being Element of L holds
( c "/\" a = a & a "/\" c = a )

proof

consider b being Element of L;
take c = (b | b) | ((b | b) | (b | b)); :: thesis: for a being Element of L holds
( c "/\" a = a & a "/\" c = a )
let a be Element of L; :: thesis: ( c "/\" a = a & a "/\" c = a )
thus c "/\" a = a :: thesis: a "/\" c = a

proof

set X = b " ;
c "/\" a = (((b | b) | ((b " ) | (b " ))) | a) " by Def12
.= (a | ((b " ) | ((b " ) | (b " )))) " by Th32
.= (a | a) " by Def14
.= a by Def13 ;
hence c "/\" a = a ; :: thesis: verum

end;

thus a "/\" c = a :: thesis: verum

proof

set X = b " ;
a "/\" c = (a | ((b | b) | ((b " ) | (b " )))) " by Def12
.= (a | a) " by Def14
.= a by Def13 ;
hence a "/\" c = a ; :: thesis: verum

end;

end;

then A2: L is upper-bounded' by Def1;
for b being Element of L ex a being Element of L st a is_a_complement'_of b

proof

let b be Element of L; :: thesis: ex a being Element of L st a is_a_complement'_of b
A3: Top' L = (b | b) | ((b | b) | (b | b))

proof

set X = (b | b) | ((b | b) | (b | b));
for a being Element of L holds
( ((b | b) | ((b | b) | (b | b))) "/\" a = a & a "/\" ((b | b) | ((b | b) | (b | b))) = a )

proof

let a be Element of L; :: thesis: ( ((b | b) | ((b | b) | (b | b))) "/\" a = a & a "/\" ((b | b) | ((b | b) | (b | b))) = a )
thus ((b | b) | ((b | b) | (b | b))) "/\" a = a :: thesis: a "/\" ((b | b) | ((b | b) | (b | b))) = a

proof

set Y = b " ;
((b | b) | ((b | b) | (b | b))) "/\" a = (((b | b) | ((b " ) | (b " ))) | a) " by Def12
.= (a | ((b " ) | ((b " ) | (b " )))) " by Th32
.= (a | a) " by Def14
.= a by Def13 ;
hence ((b | b) | ((b | b) | (b | b))) "/\" a = a ; :: thesis: verum

end;

thus a "/\" ((b | b) | ((b | b) | (b | b))) = a :: thesis: verum

proof

set Y = b " ;
a "/\" ((b | b) | ((b | b) | (b | b))) = (a | ((b | b) | ((b " ) | (b " )))) " by Def12
.= (a | a) " by Def14
.= a by Def13 ;
hence a "/\" ((b | b) | ((b | b) | (b | b))) = a ; :: thesis: verum

end;

thus verum ; :: thesis: verum

end;

hence Top' L = (b | b) | ((b | b) | (b | b)) by A2, Def2; :: thesis: verum

end;

A4: Bot' L = (b | (b | b)) | (b | (b | b))

proof

set X = (b | (b | b)) | (b | (b | b));
for a being Element of L holds
( ((b | (b | b)) | (b | (b | b))) "\/" a = a & a "\/" ((b | (b | b)) | (b | (b | b))) = a )

proof

let a be Element of L; :: thesis: ( ((b | (b | b)) | (b | (b | b))) "\/" a = a & a "\/" ((b | (b | b)) | (b | (b | b))) = a )
thus ((b | (b | b)) | (b | (b | b))) "\/" a = a :: thesis: a "\/" ((b | (b | b)) | (b | (b | b))) = a

proof

((b | (b | b)) | (b | (b | b))) "\/" a = (((b | (b | b)) " ) " ) | (a | a) by Def12
.= (((a | (a | a)) " ) " ) | (a | a) by Th33
.= (a | (a | a)) | (a | a) by Def13
.= (a | a) | (a | (a | a)) by Th32
.= (a | a) | (a | a) by Def14
.= a by Def13 ;
hence ((b | (b | b)) | (b | (b | b))) "\/" a = a ; :: thesis: verum

end;

thus a "\/" ((b | (b | b)) | (b | (b | b))) = a :: thesis: verum

proof

a "\/" ((b | (b | b)) | (b | (b | b))) = (a | a) | (((b | (b | b)) " ) " ) by Def12
.= (a | a) | (((a | (a | a)) " ) " ) by Th33
.= (a | a) | (a | (a | a)) by Def13
.= (a | a) | (a | a) by Def14
.= a by Def13 ;
hence a "\/" ((b | (b | b)) | (b | (b | b))) = a ; :: thesis: verum

end;

thus verum ; :: thesis: verum

end;

hence Bot' L = (b | (b | b)) | (b | (b | b)) by A1, Def4; :: thesis: verum

end;

set a = b | b;
take b | b ; :: thesis: b | b is_a_complement'_of b
A5: (b | b) "\/" b = ((b | b) | (b | b)) | (b | b) by Def12
.= Top' L by A3, Th32 ;
A6: b "\/" (b | b) = Top' L by A3, Def12;
A7: (b | b) "/\" b = ((b | b) | b) | ((b | b) | b) by Def12
.= (b | (b | b)) | ((b | b) | b) by Th32
.= Bot' L by A4, Th32 ;
b "/\" (b | b) = Bot' L by A4, Def12;
hence b | b is_a_complement'_of b by A5, A6, A7, Def6; :: thesis: verum

end;

then A8: L is complemented' by Def7;
A9: L is join-commutative by Th34;
A10: L is meet-commutative by Th35;
A11: L is distributive by Th36;
L is distributive' by Th37;
hence L is Boolean Lattice by A1, A2, A8, A9, A10, A11; :: thesis: verum