let X be set ; :: thesis: for x, y being Element of (BoolePoset X) holds
( x "\/" y = x \/ y & x "/\" y = x /\ y )
let x, y be Element of (BoolePoset X); :: thesis: ( x "\/" y = x \/ y & x "/\" y = x /\ y )
reconsider x = x, y = y as Element of (InclPoset (bool X)) by Th4;
( x "/\" y = x /\ y & x "\/" y = x \/ y ) by Lm1, Th8, Th9;
hence ( x "\/" y = x \/ y & x "/\" y = x /\ y ) by Th4; :: thesis: verum