let X, Y be set ; :: thesis: varcl (X \/ Y) = (varcl X) \/ (varcl Y)
set A = { (varcl a) where a is Element of {X,Y} : verum } ;
X \/ Y = union {X,Y} by ZFMISC_1:75;
then A1: varcl (X \/ Y) = union { (varcl a) where a is Element of {X,Y} : verum } by Th10;
{ (varcl a) where a is Element of {X,Y} : verum } = {(varcl X),(varcl Y)}
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {(varcl X),(varcl Y)} c= { (varcl a) where a is Element of {X,Y} : verum }
let x be object ; :: thesis: ( x in { (varcl a) where a is Element of {X,Y} : verum } implies x in {(varcl X),(varcl Y)} )
assume x in { (varcl a) where a is Element of {X,Y} : verum } ; :: thesis: x in {(varcl X),(varcl Y)}
then consider a being Element of {X,Y} such that
A2: x = varcl a ;
( a = X or a = Y ) by TARSKI:def 2;
hence x in {(varcl X),(varcl Y)} by A2, TARSKI:def 2; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(varcl X),(varcl Y)} or x in { (varcl a) where a is Element of {X,Y} : verum } )
assume x in {(varcl X),(varcl Y)} ; :: thesis: x in { (varcl a) where a is Element of {X,Y} : verum }
then ( ( x = varcl X & X in {X,Y} ) or ( x = varcl Y & Y in {X,Y} ) ) by TARSKI:def 2;
hence x in { (varcl a) where a is Element of {X,Y} : verum } ; :: thesis: verum
end;
hence varcl (X \/ Y) = (varcl X) \/ (varcl Y) by A1, ZFMISC_1:75; :: thesis: verum