let X, Y be set ; :: thesis: proj2_3 (X \/ Y) = (proj2_3 X) \/ (proj2_3 Y)
thus proj2_3 (X \/ Y) = proj2 ((proj1 X) \/ (proj1 Y)) by Th23
.= (proj2_3 X) \/ (proj2_3 Y) by Th27 ; :: thesis: verum