let A, B be non empty preBoolean set ; :: thesis: for a, b being Element of [:A,B:] holds a /\ (b \/ a) = a
let a, b be Element of [:A,B:]; :: thesis: a /\ (b \/ a) = a
thus a /\ (b \/ a) = (a /\ b) \/ (a /\ a) by Th5
.= a by Th6 ; :: thesis: verum