let V, C be set ; :: thesis: for A, B being Element of SubstitutionSet (V,C) st A ^ B = A holds
for a being set st a in A holds
ex b being set st
( b in B & b c= a )
let A, B be Element of SubstitutionSet (V,C); :: thesis: ( A ^ B = A implies for a being set st a in A holds
ex b being set st
( b in B & b c= a ) )
assume A1: A ^ B = A ; :: thesis: for a being set st a in A holds
ex b being set st
( b in B & b c= a )
let a be set ; :: thesis: ( a in A implies ex b being set st
( b in B & b c= a ) )
assume a in A ; :: thesis: ex b being set st
( b in B & b c= a )
then consider b, c being set such that
b in A and
A2: c in B and
A3: a = b \/ c by A1, SUBSTLAT:15;
take c ; :: thesis: ( c in B & c c= a )
thus ( c in B & c c= a ) by A2, A3, XBOOLE_1:7; :: thesis: verum