let V be Universe; :: thesis: for X being Subclass of V
for A, B being set st X is closed_wrt_A1-A7 & A in X & B in X holds
A /\ B in X
let X be Subclass of V; :: thesis: for A, B being set st X is closed_wrt_A1-A7 & A in X & B in X holds
A /\ B in X
let A, B be set ; :: thesis: ( X is closed_wrt_A1-A7 & A in X & B in X implies A /\ B in X )
assume that
A1: ( X is closed_wrt_A1-A7 & A in X ) and
A2: B in X ; :: thesis: A /\ B in X
A \ B in X by A1, A2, Th4;
then A \ (A \ B) in X by A1, Th4;
hence A /\ B in X by XBOOLE_1:48; :: thesis: verum