let G be Group; :: thesis: for A, B being non empty Subset of G

for N being Subgroup of G holds N ~ (A \/ B) = (N ~ A) \/ (N ~ B)

let A, B be non empty Subset of G; :: thesis: for N being Subgroup of G holds N ~ (A \/ B) = (N ~ A) \/ (N ~ B)

let N be Subgroup of G; :: thesis: N ~ (A \/ B) = (N ~ A) \/ (N ~ B)

thus N ~ (A \/ B) c= (N ~ A) \/ (N ~ B) :: according to XBOOLE_0:def 10 :: thesis: (N ~ A) \/ (N ~ B) c= N ~ (A \/ B)

assume A2: x in (N ~ A) \/ (N ~ B) ; :: thesis: x in N ~ (A \/ B)

then reconsider x = x as Element of G ;

( x in N ~ A or x in N ~ B ) by A2, XBOOLE_0:def 3;

then ( x * N meets A or x * N meets B ) by Th14;

then x * N meets A \/ B by XBOOLE_1:70;

hence x in N ~ (A \/ B) ; :: thesis: verum

for N being Subgroup of G holds N ~ (A \/ B) = (N ~ A) \/ (N ~ B)

let A, B be non empty Subset of G; :: thesis: for N being Subgroup of G holds N ~ (A \/ B) = (N ~ A) \/ (N ~ B)

let N be Subgroup of G; :: thesis: N ~ (A \/ B) = (N ~ A) \/ (N ~ B)

thus N ~ (A \/ B) c= (N ~ A) \/ (N ~ B) :: according to XBOOLE_0:def 10 :: thesis: (N ~ A) \/ (N ~ B) c= N ~ (A \/ B)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (N ~ A) \/ (N ~ B) or x in N ~ (A \/ B) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in N ~ (A \/ B) or x in (N ~ A) \/ (N ~ B) )

assume A1: x in N ~ (A \/ B) ; :: thesis: x in (N ~ A) \/ (N ~ B)

then reconsider x = x as Element of G ;

x * N meets A \/ B by A1, Th14;

then ( x * N meets A or x * N meets B ) by XBOOLE_1:70;

then ( x in N ~ A or x in N ~ B ) ;

hence x in (N ~ A) \/ (N ~ B) by XBOOLE_0:def 3; :: thesis: verum

end;assume A1: x in N ~ (A \/ B) ; :: thesis: x in (N ~ A) \/ (N ~ B)

then reconsider x = x as Element of G ;

x * N meets A \/ B by A1, Th14;

then ( x * N meets A or x * N meets B ) by XBOOLE_1:70;

then ( x in N ~ A or x in N ~ B ) ;

hence x in (N ~ A) \/ (N ~ B) by XBOOLE_0:def 3; :: thesis: verum

assume A2: x in (N ~ A) \/ (N ~ B) ; :: thesis: x in N ~ (A \/ B)

then reconsider x = x as Element of G ;

( x in N ~ A or x in N ~ B ) by A2, XBOOLE_0:def 3;

then ( x * N meets A or x * N meets B ) by Th14;

then x * N meets A \/ B by XBOOLE_1:70;

hence x in N ~ (A \/ B) ; :: thesis: verum