let C be initialized ConstructorSignature; :: thesis: for f being valuation of C
for A, B being Subset of (QuasiAdjs C) holds (A \/ B) at f = (A at f) \/ (B at f)
let f be valuation of C; :: thesis: for A, B being Subset of (QuasiAdjs C) holds (A \/ B) at f = (A at f) \/ (B at f)
let A, B be Subset of (QuasiAdjs C); :: thesis: (A \/ B) at f = (A at f) \/ (B at f)
thus (A \/ B) at f c= (A at f) \/ (B at f) :: according to XBOOLE_0:def 10 :: thesis: (A at f) \/ (B at f) c= (A \/ B) at f
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (A \/ B) at f or x in (A at f) \/ (B at f) )
assume x in (A \/ B) at f ; :: thesis: x in (A at f) \/ (B at f)
then consider a being quasi-adjective of C such that
A1: x = a at f and
A2: a in A \/ B ;
( a in A or a in B ) by A2, XBOOLE_0:def 3;
then ( x in A at f or x in B at f ) by A1;
hence x in (A at f) \/ (B at f) by XBOOLE_0:def 3; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (A at f) \/ (B at f) or x in (A \/ B) at f )
assume x in (A at f) \/ (B at f) ; :: thesis: x in (A \/ B) at f
then ( x in A at f or x in B at f ) by XBOOLE_0:def 3;
then ( ( A c= A \/ B & ex a being quasi-adjective of C st
( x = a at f & a in A ) ) or ( B c= A \/ B & ex a being quasi-adjective of C st
( x = a at f & a in B ) ) ) by XBOOLE_1:7;
hence x in (A \/ B) at f ; :: thesis: verum