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 Th20
.= a by Th21 ; :: thesis: verum