let F1, F2 be Field of BL; :: thesis: ( A c= F1 & ( for F being Field of BL st A c= F holds
F1 c= F ) & A c= F2 & ( for F being Field of BL st A c= F holds
F2 c= F ) implies F1 = F2 )
assume ( A c= F1 & ( for F being Field of BL st A c= F holds
F1 c= F ) & A c= F2 & ( for F being Field of BL st A c= F holds
F2 c= F ) ) ; :: thesis: F1 = F2
hence ( F1 c= F2 & F2 c= F1 ) ; :: according to XBOOLE_0:def 10 :: thesis: verum