let X, Y be set ; :: thesis: proj1_4 (X \/ Y) = (proj1_4 X) \/ (proj1_4 Y)
thus proj1_4 (X \/ Y) = proj1 ((proj1_3 X) \/ (proj1_3 Y)) by Th31
.= (proj1_4 X) \/ (proj1_4 Y) by Th23 ; :: thesis: verum