let Q be multLoop; :: thesis: for x being Element of Q holds
( x in Nucl Q iff ( x in Nucl_l Q & x in Nucl_m Q & x in Nucl_r Q ) )
let x be Element of Q; :: thesis: ( x in Nucl Q iff ( x in Nucl_l Q & x in Nucl_m Q & x in Nucl_r Q ) )
thus ( x in Nucl Q implies ( x in Nucl_l Q & x in Nucl_m Q & x in Nucl_r Q ) ) :: thesis: ( x in Nucl_l Q & x in Nucl_m Q & x in Nucl_r Q implies x in Nucl Q )
proof
assume A1: x in Nucl Q ; :: thesis: ( x in Nucl_l Q & x in Nucl_m Q & x in Nucl_r Q )
then x in (Nucl_l Q) /\ (Nucl_m Q) by XBOOLE_0:def 4;
hence ( x in Nucl_l Q & x in Nucl_m Q & x in Nucl_r Q ) by XBOOLE_0:def 4, A1; :: thesis: verum
end;
assume that
A2: ( x in Nucl_l Q & x in Nucl_m Q ) and
A3: x in Nucl_r Q ; :: thesis: x in Nucl Q
x in (Nucl_l Q) /\ (Nucl_m Q) by XBOOLE_0:def 4, A2;
hence x in Nucl Q by XBOOLE_0:def 4, A3; :: thesis: verum